$\forall$$T_{1}$, $T_{2}$:Type, ${\it as}$:($T_{1}$ List), ${\it bs}$:($T_{2}$ List). zip(${\it as}$;${\it bs}$) $\in$ ((:$T_{1}$ $\times$ $T_{2}$) List)